Metaprogramming in Lean 4
Lean4はElaborationという強力なメタプログラミングの機能があり、コンパイラフロントエンド自体が大体このElaborationを使ってかかれている。この記事はその概略が書いてある ref この事実をふまえ、Leanは証明にirreducibleとタグ付けする。ファイルを処理するとき、このタグはパーサー(より正確にはelaborator)に対して、「このタグが付いたものを展開する必要はない」というヒントとして機能する。 ref Leanには暗黙の引数を推論するための非常に複雑なメカニズムがあり、それを使うと関数型や述語、さらには証明を推論できることを見ていく。このような「穴」または「プレースホルダー」を埋めるプロセスは、elaborationとしてよく知られている。暗黙の引数の存在により、ある式の意味を正確に確定させるための情報が不十分である状況が起こりうる。id や List.nil のような表現は、文脈によって異なる意味を持つことがあるため、polymorphic(多相的)であると言われる。ref